Inference at * 2 0 
Iof proof for Lemma multiply nat wf:

.....set predicate..... NILNIL

1. i : 
2. j : 
  0  (i * j) 

latex

 by (%S% \p.AbSetHD (get_int_arg `hn` p) p) 

latex

 1: 

 1: 2. j : 
 1: 3. j  0 
 1:   0  (i * j)
 .

Definitions	, f(a), s = t, n * m, #$n, x:AB(x), A  B, {x:A| B(x)} , x:A. B(x), i  j , t  T,
Lemmas	nat properties